﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Pex.Framework;
using System.Collections;
using Microsoft.Pex.Framework.Goals;

namespace MicroBenchmarks.DataStructures
{
    /// <summary>
    /// Checks common datastructure hashtable
    /// </summary>
    [PexClass]
    [PexMe.Attribute.FieldAccessObserver]
    [PexMe.Attribute.InsufficientObjectFactoryObserver]
    public partial class HashTableTest
    {
        /// <summary>
        /// Pex running without PexMe
        /// </summary>
        /// <param name="hashtable"></param>
        [PexMethod]
        [PexAssertReachEventually]
        public void HashTableSizeTest([PexAssumeUnderTest]Hashtable hashtable)
        {
            if (hashtable.Count == 1)
                PexAssert.ReachEventually();
        }

        /// <summary>
        /// Problem with Pex, not invoking LogExplorableInsufficiency
        /// </summary>
        /// <param name="hashtable"></param>
        [PexMethod]
        [PexAssertReachEventually]
        public void HashTableKeyTest1([PexAssumeUnderTest]Hashtable hashtable)
        {
            if (hashtable.ContainsKey("test"))
                PexAssert.ReachEventually();
        }

        /// <summary>
        /// Problem with Pex, not invoking LogExplorableInsufficiency
        /// </summary>
        /// <param name="hashtable"></param>
        /// <param name="key"></param>
        [PexMethod]
        [PexAssertReachEventually]
        public void HashTableKeyTest2([PexAssumeUnderTest]Hashtable hashtable, string key)
        {
            if (hashtable.ContainsKey(key))
                PexAssert.ReachEventually();
        }

        /// <summary>
        /// Pex working fine without the help of PexMe
        /// </summary>
        /// <param name="hashtable"></param>
        [PexMethod]
        [PexAssertReachEventually]
        public void HashTableValueTest1([PexAssumeUnderTest]Hashtable hashtable)
        {
            if (hashtable.ContainsValue("test"))
                PexAssert.ReachEventually();
        }

        /// <summary>
        /// Pex working fine without the help of PexMe
        /// </summary>
        /// <param name="hashtable"></param>
        [PexMethod]
        [PexAssertReachEventually]
        public void HashTableValueTest2([PexAssumeUnderTest]Hashtable hashtable, string value)
        {
            if (hashtable.ContainsValue(value))
                PexAssert.ReachEventually();
        }

        /// <summary>
        /// Pex working fine without the help of PexMe
        /// </summary>
        /// <param name="hashtable"></param>
        [PexMethod]
        [PexAssertReachEventually]
        public void HashTableIteratorTest([PexAssumeUnderTest]Hashtable hashtable)
        {
            foreach (var value in hashtable.Values)
                PexAssert.ReachEventually();
        }
    }
}
